Termination Proof Script

Consider the TRS R consisting of the rewrite rules

There are 5 dependency pairs:

The approximated dependency graph contains one SCC: {5-9}.

Consider the SCC {5-9}. By taking the AF π with π(a__f) = π(A__F) = π(f) = π(mark) = π(MARK) = 1 together with the lexicographic path order with empty precedence, the rules in {2-4,7,8} are weakly decreasing and the rules in {1,5,6,9} are strictly decreasing. There is one new SCC.
- Consider the SCC {8}. There are no usable rules. By taking the AF π with π(MARK) = 1 and π(f) = [1] together with the lexicographic path order with empty precedence, rule 8 is strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.05 seconds) --- May 4, 2006